Issue2423.agda:24,8-10
Cannot eliminate type  S  with projection  S._.f
when checking that the clause test s .f = s .f has type S → S
